Search Results

Documents authored by Dezani-Ciancaglini, Mariangiola

Document
DOI: 10.4230/OASIcs.Gabbrielli.3
Deconfined Intersection Types in Java

Authors: Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
We show how Java intersection types can be freed from their confinement in type casts, in such a way that the proposed Java extension is safe and fully compatible with the current language. To this aim, we exploit two calculi which formalise the simple Java core and the extended language, respectively. Namely, the second calculus extends the first one by allowing an intersection type to be used anywhere in place of a nominal type. We define a translation algorithm, compiling programs of the extended language into programs of the former calculus. The key point is the interaction between λ-expressions and intersection types, that adds safe expressiveness while being the crucial matter in the translation. We prove that the translation preserves typing and semantics. Thus, typed programs in the proposed extension are translated to typed Java programs. Moreover, semantics of translated programs coincides with the one of the source programs.
Cite as

Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. Deconfined Intersection Types in Java. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dezaniciancaglini_et_al:OASIcs.Gabbrielli.3,
  author =	{Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Venneri, Betti},
  title =	{{Deconfined Intersection Types in Java}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{3:1--3:25},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.3},
  URN =		{urn:nbn:de:0030-drops-132256},
  doi =		{10.4230/OASIcs.Gabbrielli.3},
  annote =	{Keywords: Intersection Types, Featherweight Java, Lambda Expressions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.30
Concurrent Reversible Sessions

Authors: Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We present a calculus for concurrent reversible multiparty sessions, which improves on recent proposals in several respects: it allows for concurrent and sequential composition within processes and types, it gives a compact representation of the past of processes and types, which facilitates the definition of rollback, and it implements a fine-tuned strategy for backward computation. We propose a refined session type system for our calculus and show that it enforces the expected properties of session fidelity, forward and backward progress, as well as causal consistency. In conclusion, our calculus is a conservative extension of previous proposals, offering enhanced expressive power and refined analysis techniques.
Cite as

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Concurrent Reversible Sessions. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{castellani_et_al:LIPIcs.CONCUR.2017.30,
  author =	{Castellani, Ilaria and Dezani-Ciancaglini, Mariangiola and Giannini, Paola},
  title =	{{Concurrent Reversible Sessions}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{30:1--30:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.30},
  URN =		{urn:nbn:de:0030-drops-77877},
  doi =		{10.4230/LIPIcs.CONCUR.2017.30},
  annote =	{Keywords: Communication-centric Systems, Reversible Computation, Process Calculi, Multiparty Session Types}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2013.129
Isomorphism of "Functional" Intersection Types

Authors: Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
Type isomorphism for intersection types is quite odd, since it is not a congruence and it does not extend type equality in the standard interpretation of types. The lack of congruence is due to the proof theoretic nature of the intersection introduction rule, which requires the same term to be the subject of both premises. A partial congruence can be recovered by introducing a suitable notion of type similarity. Type equality in standard models becomes included in type isomorphism whenever atomic types have "functional" interpretations, i.e. they are equivalent to arrow types. This paper characterises type isomorphism for a type system in which the equivalence between atomic types and arrow types is induced by the initial projections of the Scott's model via the correspondence between inverse limit models and filter lambda-models.
Cite as

Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi. Isomorphism of "Functional" Intersection Types. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 129-149, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{coppo_et_al:LIPIcs.TYPES.2013.129,
  author =	{Coppo, Mario and Dezani-Ciancaglini, Mariangiola and Margaria, Ines and Zacchi, Maddalena},
  title =	{{Isomorphism of "Functional" Intersection Types}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{129--149},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.129},
  URN =		{urn:nbn:de:0030-drops-46296},
  doi =		{10.4230/LIPIcs.TYPES.2013.129},
  annote =	{Keywords: Type Isomorphism, Lambda calculus, Intersection Types}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact